STM: ecl-subtype

ABS: ecl-halt(ds;da;x)

STM: ecl-halt wf

STM: ecl-halt-nil

STM: ecl-halt-unique

ABS: ecl-halt-kind(x)

STM: ecl-halt-kind wf

STM: ecl-halt-kind-last

ABS: ecl-halt-type(da;x)

STM: ecl-halt-type wf

STM: ecl-halt-type-last

ABS: ecl-act(ds;da;m;x)

STM: ecl-act wf

STM: ecl-act-halt

STM: ecl-act-nil

ABS: ecl-trans-tuple{i:l}(ds;da)

STM: ecl-trans-tuple wf

ABS: ecl-trans-type(A)

STM: ecl-trans-type wf

ABS: ecl-trans-state-from(v;z;L)

STM: ecl-trans-state-from wf

ABS: ecl-trans-init(v)

STM: ecl-trans-init wf

ABS: ecl-trans-h(v)

STM: ecl-trans-h wf

ABS: ecl-trans-ks(v)

STM: ecl-trans-ks wf

ABS: ecl-trans-a(v)

STM: ecl-trans-a wf

ABS: ecl-trans-state(v;L)

STM: ecl-trans-state wf

ABS: ecl-trans-es(v)

STM: ecl-trans-es wf

STM: ecl-trans-state-from-append

STM: ecl-trans-state-append

ABS: ecl-trans-reachable(ds;da;v;L;x)

STM: ecl-trans-reachable wf

ABS: ecl-trans-normal(x)

STM: ecl-trans-normal wf

ABS: combine-ecl-tuples(A;B;f;g)

STM: combine-ecl-tuples wf

ABS: combine-halt-info(ea;eb;f;g;x)

STM: combine-halt-info wf

ABS: combine-ecl-tuples2(A;B;f;g)

STM: combine-ecl-tuples2 wf

STM: combine-ecl-trans-state0

STM: combine-ecl-trans-state1

STM: ecl-normal-combine

STM: ecl-normal-combine2

ABS: reset-ecl-tuple(A)

STM: reset-ecl-tuple wf

ABS: add-ecl-act(A;m)

STM: add-ecl-act wf

ABS: ecl-base-tuple(k;test)

STM: ecl-base-tuple wf

ABS: ecl-add-throw(A;m)

STM: ecl-add-throw wf

ABS: ecl-add-catch(A;l)

STM: ecl-add-catch wf

ABS: ecl-kinds(x)

STM: ecl-kinds wf

ABS: ecl-trans(x)

STM: ecl-trans wf

STM: ecl-kinds-ecl-trans

ABS: ecl-trans-halt2(ds;da;A)

STM: ecl-trans-halt2 wf

STM: ecl-trans-halt2-bound

STM: combine-ecl-trans-state2

ABS: ecl-trans-act(ds;da;A)

STM: ecl-trans-act wf

STM: ecl-trans-act-last

STM: ecl-trans-act-nil

STM: ecl-trans-act functionality

STM: ecl-trans-act-functionality2

STM: ecl-reset-lemma

STM: ecl-reset-state

STM: ecl-reset-init

STM: ecl-reset-halt

STM: ecl-trans-halt2-add-catch

STM: ecl-trans-halt2-add-throw

STM: ecl-trans-property

ABS: ecl-max(x)

STM: ecl-max wf

ABS: ecl-ex(x)

STM: ecl-ex wf

STM: ecl-halt-ex

ABS: ecl-es-halt(es;x)

STM: ecl-es-halt wf

STM: ecl-es-halt-ecl-halt

ABS: ecl-es-act(es;m;x)

STM: ecl-es-act wf

STM: ecl-es-act-ecl-act

STM: decidable ecl-es-act

STM: decidable ecl-es-halt

ABS: action[[a n]][e1;e2]

STM: es-bact wf

STM: assert-es-bact

ABS: msg-item(ds;da;k;l)

STM: msg-item wf

ABS: msg-spec(ds;da)

STM: msg-spec wf

ABS: msg-spec-links(snd)

STM: msg-spec-links wf

ABS: msg-spec-loc(snd;i)

STM: msg-spec-loc wf

ABS: msg-spec-loc-decl(snd;i;da)

STM: msg-spec-loc-decl wf

STM: msg-spec-loc-decl-implies

ABS: k sends on l with tag tg [s,v.f(s;v)], at marker n

STM: msg-spec1 wf

ABS: a  b

STM: msg-spec-join wf

STM: msg-spec-links-spec1

STM: msg-spec-loc-spec1

STM: msg-spec-loc-decl-spec1

STM: msg-spec-loc-empty

STM: msg-spec-loc-decl-join

ABS: ecl-tags(l;snd)

STM: ecl-tags wf

STM: member-ecl-tags

STM: no repeats-ecl-tags

STM: ecl-tags-spec1

ABS: update-spec(ds;da)

STM: update-spec wf

ABS: update-spec-vars(upd)

STM: update-spec-vars wf

ABS: update-spec-dom(upd;k;x)

STM: update-spec-dom wf

ABS: update-spec-decl(upd;ds)

STM: update-spec-decl wf

ABS: update-spec1(k;x;n;s,v.f(s;v))

STM: update-spec1 wf

STM: update-spec1 wf2

ABS: a  b

STM: update-spec-join wf

STM: update-spec-join-vars

STM: update-spec-join-decl

STM: update-spec1-decl

STM: update-spec-empty-decl

ABS: @i[[x;snd]]

STM: ecl-mng-sends wf

STM: ecl-mng-sends-single

ABS: @i[[x;upd]]

STM: ecl-mng-update wf

ABS: @i[[x;snd;upd]]

STM: ecl-mng wf

ABS: ecl-machine1{$ecl:ut2}(i; ds; da; A)

STM: ecl-machine1 wf

STM: ecl-machine1-realizes

ABS: ecl-machine2(i;ds;da;x;T;ks;a;upd)

STM: ecl-machine2 wf

STM: ecl-machine2-realizes

STM: ecl-machine2-loc

ABS: ecl-m3(a;snd;x;l)

STM: ecl-m3 wf

ABS: ecl-machine3(ds;da;x;T;ks;a;snd)

STM: ecl-machine3 wf

STM: ecl-machine3-realizes

STM: ecl-machine3-loc

ABS: esp-machine at i with state $eclAstate variables dsactions dasends sndupdates upd

STM: ecl-machine wf

STM: ecl-2-3-compat

STM: ecl-1-2-compat

STM: ecl-1-3-compat

STM: ecl-realizes

STM: ecl-feasible

STM: ecl-machine-loc

STM: ecl-machine-R-da

STM: ecl-machine-R-da-dom

STM: ecl-machine-icompat

STM: ecl-disjoint-compatible

STM: ecl-precond-compatible

STM: ecl-effect-compatible

STM: es-sends-iff-bact

STM: ecl-mng-sends-single2

STM: duplicate-and

STM: ecl-es-halt-example1